/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.subscope;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;

import alloy.ast.LeafId;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.util.Dbg;

/**
 * A representation of a relation annotation, a sequence of arity-1 {@link LeafId leaf ids}.
 * The annotation essentially corresponds to the relations represented by each id arrowed together,
 * eg. the anotation (A,B,C) represents the relation A -> B -> C.  Provides methods for quickly accessing
 * different columns of the annotations and comparing annotations (to see if they intersect, if one
 * is contained in the other, etc.).  RelAnnotations are immutable.
 * <p>
 * RelANnotations are made Comparable so we can use them in TreeSets and TreeMaps.
 */
public final class RelAnnotation implements Comparable {

    /** the sequence of {@link LeafIds}s comprising the annotation */
    private List /* of LeafId */ _ids;

    /** information about the signature hierarchy */
    private ScopedSigsInfo _scopedSigsInfo;

    private final int _hashcode;
    
    public RelAnnotation(LeafId id,
                         ScopedSigsInfo scopedSigsInfo_) {
        this(Collections.singletonList(id), scopedSigsInfo_);
    }

    private RelAnnotation(List ids_,
                         ScopedSigsInfo scopedSigsInfo_) {
        this._ids = ids_;
        this._scopedSigsInfo = scopedSigsInfo_;
	int hcode = 0;
        for (int i = 0; i < ids_.size(); i++) {
            hcode += ((LeafId)ids_.get(i)).hashCode();
        }
	this._hashcode = hcode;
    }
                          
    /** @return the arity of this */
    public int arity() {
        return _ids.size();
    }

    /** @return the leaf id at column i_ */
    public LeafId relIdAt(int i_) {
        return (LeafId)_ids.get(i_);
    }

    /**
     * Compare this RelAnnotation to the given RelAnnotation.
     * The comparison is done lexicographically.
     */
    public int compareTo(Object obj_) {
	Dbg.chk(obj_!=null && obj_ instanceof RelAnnotation);
	RelAnnotation that = (RelAnnotation)obj_;
	if (this.arity() < that.arity()) return -1;
	if (this.arity() > that.arity()) return +1;
	for (int i=0; i<arity(); i++) {
	    int compareIds = this.relIdAt(i).compareTo(that.relIdAt(i));
	    if (compareIds != 0)
		return compareIds;
	}
	return 0;
    }

    /** @return <code>true</code> if this is contained in other_; <code>false</code>
     * otherwise.  Assumes both RelAnnotations have the same type. */
    public boolean in(RelAnnotation other_) {
        Dbg.chk(arity() == other_.arity());
        // otherwise, each column of this must be contained in the corresponding
        // column of other_
        for (int col = 0; col < arity(); col++) {
            LeafId myId = relIdAt(col);
            LeafId otherId = other_.relIdAt(col);
            if (!_scopedSigsInfo.extendsOrEquals(myId, otherId)) return false;
        }
        return true;
    }

    /** @return <code>true</code> if this intersects other_; <code>false</code>
        otherwise. Assumes both RelAnnotations have the same type. */ 
    public boolean intersects(RelAnnotation other_) {
        Dbg.chk(arity() == other_.arity());
        // otherwise, intersect if no column is disjoint, which in our
        // case means one column is contained in the other
        for (int col = 0; col < arity(); col++) {
            LeafId myId = relIdAt(col);
            LeafId otherId = other_.relIdAt(col);
            if (!(_scopedSigsInfo.extendsOrEquals(myId, otherId) ||
                  _scopedSigsInfo.extendsOrEquals(otherId, myId))) return false;
        }
        return true;
    }

    public RelAnnotation product(RelAnnotation other_) {
        List prodIds = new ArrayList(_ids);
        prodIds.addAll(other_._ids);
        return new RelAnnotation(prodIds, _scopedSigsInfo);
    }
    
    public static RelAnnotation fromType(RelationType type_, ScopedSigsInfo scopedSigsInfo_) {
        List /* of LeafId */ ids = new ArrayList();
        for (int i = 0; i < type_.numBasicTypes(); i++) {
            ids.add(_idForBasicType(type_.getBasicTypeAt(i)));
        }
        return new RelAnnotation(ids, scopedSigsInfo_);
    }        

    private static LeafId _idForBasicType(BasicType basType_) {
        return
	    //(basType_ instanceof IntType) ?
	    //LeafId.INT_ID :
        ((SigType)basType_).getSignature().getLeafId();
    }

    public boolean equals(Object obj_) {
        if (!(obj_ instanceof RelAnnotation)) return false;
        RelAnnotation other = (RelAnnotation)obj_;
        int arity = arity();
        if (arity != other.arity()) return false;
        boolean foundDiff = false;
        for (int i = 0; i < arity && !foundDiff; i++) {
            foundDiff |= relIdAt(i).equals(other.relIdAt(i));
        }
        return !foundDiff;
    }

    public int hashCode() {
        return _hashcode;
    }

    public RelAnnotation fromColumn(int column_) {
        return new RelAnnotation((LeafId)_ids.get(column_), _scopedSigsInfo);
    }

    public RelAnnotation withoutColumn(int column_) {
        List resultIds = new ArrayList(_ids);
        resultIds.remove(column_);
        return new RelAnnotation(resultIds, _scopedSigsInfo);
    }
    
    public RelAnnotation join(RelAnnotation other_) {
        // first, check if join column can intersect, and
        // if not, return null
        LeafId myJoinId = relIdAt(arity() - 1);
        LeafId otherJoinId = other_.relIdAt(0);
        if (!(_scopedSigsInfo.extendsOrEquals(myJoinId, otherJoinId) ||
              _scopedSigsInfo.extendsOrEquals(otherJoinId, myJoinId))) {
            return null;
        }
        List resultIds = new ArrayList();
        for (int i = 0; i < arity() - 1; i++) {
            resultIds.add(relIdAt(i));
        }
        for (int i = 1; i < other_.arity(); i++) {
            resultIds.add(other_.relIdAt(i));
        }
        return new RelAnnotation(resultIds, _scopedSigsInfo);
    }

    public RelAnnotation transpose() {
        Dbg.chk(arity() == 2);
        List resultIds = new ArrayList(_ids);
        Collections.reverse(resultIds);
        return new RelAnnotation(resultIds, _scopedSigsInfo);
    }

    public String toString() {
        StringBuffer ret = new StringBuffer();
        for (Iterator idIter = _ids.iterator(); idIter.hasNext(); ) {
            ret.append(_scopedSigsInfo.getScopedSigName((LeafId)idIter.next()));
            if (idIter.hasNext()) {
                ret.append(" -> ");
            }
        }
        return ret.toString();
    }
}
